#editor {
	border: 0;
	font-family: "Monaco", "Consolas", "Bitstream Vera Sans Mono", monospace;
}

#editor {
	font-size: 12px;
	color: #eeeeee;
	background-color: #303030;
}

#find-results {
	font-size: 10px;
	background-color: #CDD5E1;
	border-top: 1px solid #B0B0B0;
}

#warning-banner {
	background-color: #FDEEA9;
	border-bottom: 1px solid #B0B0B0;
}
